STM: mul assoc

STM: mul wf nzero

STM: mul nzero

STM: mul add distrib

ABS: sign(x)

STM: sign wf

STM: sign-absval

STM: sign-squared

STM: gcd-reduce

ABS: gcd_reduce(p;q)

STM: gcd reduce wf

STM: gcd reduce property

STM: coprime-equiv-unique

STM: coprime-equiv-unique-pair

ABS: isint(z;a;b)

ABS: isint pair compseq tag def

ABS: isatom2(z;a;b)

ABS: isatom2 pair compseq tag def

STM: isint-int

STM: tunion wf

ABS: A  B

STM: b-union wf

ABS: qeq(r;s)

STM: qeq wf

STM: qeq-equiv

ABS: 

STM: rationals wf

STM: int-rational

STM: int inc rationals

STM: qeq-wf

ABS: r + s

STM: qadd wf

STM: qadd-add

ABS: r * s

STM: qmul wf

STM: qmul-mul

STM: qminus-minus

ABS: 1/r

STM: qinv wf

ABS: qpositive(r)

STM: qpositive wf

ABS: qrep(r)

STM: qrep wf

STM: qeq wf2

STM: assert-qeq

STM: int-eq-in-rationals

ABS: (r/s)

STM: qdiv wf

ABS: r - s

STM: qsub wf

STM: q-elim

STM: qmul ident

STM: qmul com

STM: qmul assoc

STM: qmul inv

STM: qmul inv l

STM: qadd ident

STM: qadd com

STM: qadd assoc

STM: qadd minus

STM: q distrib

STM: qmul positive

STM: qadd positive

STM: qminus positive

STM: q trichotomy

ABS: q_le(r;s)

STM: q le wf

ABS: <+>

STM: qadd grp wf

STM: mon assoc q

STM: mon ident q

STM: qinverse q

STM: qinv thru op q

STM: qinv inv q

STM: qinv id q

STM: qinv assoc q

STM: qadd inv assoc q

STM: qadd comm q

STM: qadd ac 1 q

STM: qadd grp wf2

ABS: r < s

ABS: r  s

STM: qle iff lt or eq qorder

STM: qless is sp of leq a qorder

STM: qless trans qorder

STM: qless irreflexivity qorder

STM: qless transitivity 2 qorder

STM: qless transitivity 1 qorder

STM: qle weakening eq qorder

STM: qle weakening lt qorder

STM: qle transitivity qorder

STM: qle antisymmetry qorder

STM: qless complement qorder

STM: qle complement qorder

STM: qless trichot qorder

STM: grp op preserves le qorder

STM: grp op preserves lt qorder

STM: qless irreflexivity

STM: qle antisymmetry

ABS: <+*>

STM: qrng wf

STM: qmul over plus qrng

STM: qmul over minus qrng

STM: qmul zero qrng

STM: qmul assoc qrng

STM: qmul one qrng

STM: qmul comm qrng

STM: qmul ac 1 qrng

STM: qdiv-self

STM: qmul-ident-div

STM: qmul-zero-div

STM: qmul-qdiv-cancel

STM: qmul-qdiv-cancel2

STM: qmul-qdiv-cancel3

STM: qmul-qdiv-cancel4

STM: qmul-preserves-eq

STM: test-q-norm-conv

ABS: |r|

STM: qabs wf

STM: qpositive-qabs

STM: qabs-zero

STM: qabs-squared

STM: qminus-qsub

STM: qsub-zero

STM: qsub-sub

STM: qless wf

STM: qless transitivity

STM: qless-int

STM: qle wf

STM: qle-int

ABS: a  b

STM: qge wf

ABS: a > b

STM: qgt wf

STM: qle-iff

STM: assert-qpositive

STM: qmul-positive

STM: qminus-positive

STM: decidable equal rationals

STM: decidable qle

STM: decidable qless

ABS: q_less(a;b)

STM: q less wf

STM: assert-q less

STM: assert-q less-eq

STM: assert-q le

STM: assert-q le-eq

STM: qmul-zero

STM: qmul-non-neg

STM: non-neg-qmul

STM: q-square-non-neg

STM: qadd preserves qless

STM: qadd preserves qle

STM: qadd preserves eq

STM: qmul preserves qless

STM: qmul preserves qle

STM: qadd functionality wrt qle

STM: qadd functionality wrt qless

STM: qadd functionality wrt qless 2

STM: qle functionality wrt implies

STM: qless functionality wrt implies 1

STM: qmul functionality wrt qle

STM: qmul-qdiv

STM: qless-minus

STM: qle-minus

STM: qinv-positive

STM: qinv-negative

STM: qinv-zero

STM: qdiv-qdiv

STM: q-ineq-test

STM: qadd-non-neg

ABS: qdist(r;s)

STM: qdist wf

ABS: a  b  c

STM: qbetween wf

ABS: a < b < c

STM: q-between wf

STM: qle-normalize

STM: qle reflexivity

STM: qbetween-qdist

ABS: a  j < b. E(j)

STM: qsum wf

ABS: r  n

STM: qexp wf

STM: exp zero q

STM: exp unroll q

STM: sum unroll base q

STM: sum unroll hi q

STM: sum unroll unit q

STM: sum unroll lo q

STM: sum shift q

STM: sum split q

STM: sum plus q

STM: prod sum l q

STM: prod sum r q

STM: binomial q

STM: sum of geometric prog q

STM: qsum-int

STM: qsum-qle

ABS: delta(i;j)

STM: delta wf

STM: qsum-delta

STM: summand-qle-sum

STM: qexp-positive

STM: qexp-one

STM: qsum-const

STM: qsum-const2

STM: q-geometric-series

STM: qsum-reciprocal-squares

STM: qsum-reciprocal-squares-bound

STM: q-archimedean

STM: qsum-non-neg

STM: qsum-non-neg2

STM: qsum-subsequence-qle

STM: q-not-limit-zero-diverges

STM: q-not-limit-zero-diverges-2

STM: q-min-exists

STM: q-max-exists

ABS: q-linear(k;i.X(i);y)

STM: q-linear wf

STM: q-linear-base

STM: q-linear-unroll

STM: q-linear-sum

STM: q-linear-times

STM: q-linear-equal

ABS: q-rel(r;x)

STM: q-rel wf

STM: decidable q-rel

ABS: q-rel-lub(r1;r2)

STM: q-rel-lub wf

STM: q-constraint-times

STM: q-constraint-sum

STM: q-constraint-zero

STM: q-constraint-positive

STM: q-constraint-negative

ABS: q-constraints(k;A;y)

STM: q-constraints wf

STM: product-map

STM: null-map

STM: average-qbetween

STM: average-q-between

STM: rational-has-value

ABS: as[i]?a

STM: select? wf

ABS: normalize-constraint(k;p)

STM: normalize-constraint wf

STM: normalize-constraint-eq

ABS: normalize-constraints(k;A)

STM: normalize-constraints wf

STM: normalize-constraints-eq

STM: decidable q-constraints

STM: decidable q-constraints cv

STM: decidable q-constraints-opt

ABS: qdot(as;bs)

STM: qdot wf

ABS: q-sat-constraints(k;A;y)

STM: q-sat-constraints wf

STM: decidable q-constraints2

STM: test23

ABS: test_case1()

STM: test case1 wf

STM: int nzero-rational